using System;
using System.Threading;
using System.IO;
using System.Collections.Generic;
using System.Collections;


public class RewriteResult{
	Object res;
	Dictionary<string,Object> vars;
	public RewriteResult (Object res, Dictionary<string, Object> vars)
	{
		this.res = res;
		this.vars = vars;
	}
	public Object Res {
		get {
			return this.res;
		}
		set {
			res = value;
		}
	}
	public Dictionary<string, Object> Vars {
		get {
			return this.vars;
		}
	}
}

	public class Rewrite{
		//Node cond;
		Object src;
		Object target;
		public Rewrite (Object src, Object target)
		{
			this.src = src;
			this.target = target;
		}
		public Object Src {
			get {
				return this.src;
			}
		}

		public Object Target {
			get {
				return this.target;
			}
		}	
	    public override string ToString(){
		  return "(= "+Node.nodeString(src)+" "+Node.nodeString(target)+")";
	    }
	
	
		
		
	
	public static bool isVar(Object nodeOrAtom){
		//return "x".Equals(nodeOrAtom) || "y".Equals(nodeOrAtom) || "z".Equals(nodeOrAtom);
		if( !(nodeOrAtom is string) ){
			return false;
		}
		var s = (string)nodeOrAtom;
		if( s.Length!=1 ){
			return false;
		}
		return s[0] >= 'a' && s[0] <= 'z';
	}
	
	public static HashSet<string> findFreeVars(Object pattern){
		HashSet<string> all = new HashSet<string>();
		findFreeVars(pattern, all);
		return all;
	}

	static void findFreeVars(Object pattern, HashSet<string> all){
		if( isVar(pattern) ){
			all.Add((string)pattern);
		}
		if( !(pattern is Node) ){
			return;
		}
		Node n = (Node)pattern;
		foreach( Object ch in n.Children ){
			findFreeVars(ch, all);
		}
	}

	static bool unify(Object queObj, Object rulesSrc, Dictionary<string,Object> alreadyBound){
		if( isVar(rulesSrc) ){
			String varStr = (string)rulesSrc;
			if( alreadyBound.ContainsKey(varStr) ){
				if( ! Node.eq(alreadyBound[varStr], queObj) ){
					return false;
				}
			}else{
				alreadyBound[varStr] = queObj;
			}
			return true;
		}
		if( rulesSrc is string ){
			return rulesSrc.Equals(queObj);
		}
		if( !(queObj is Node) ){
			return false;
		}
		Node que = (Node)queObj;
		if( !((Node)rulesSrc).Name.Equals(que.Name) ){
			return false;
		}
		ArrayList ruleChld = ((Node)rulesSrc).Children;
		var queChld = que.Children;
		if( ruleChld.Count != queChld.Count ){
			return false;
		}
		for( int i=0; i<ruleChld.Count; i++ ){
			if( ruleChld[i] is Node ){
				if( !(queChld[i] is Node) ){
					return false;
				}else{
					if( !unify ((Node)queChld[i], (Node)ruleChld[i], alreadyBound) ){
						return false;
					}
				}
			}else if( isVar(ruleChld[i]) ){
				String varStr = (string)ruleChld[i];
				if( alreadyBound.ContainsKey(varStr) ){
					if( ! Node.eq(alreadyBound[varStr], queChld[i]) ){
						return false;
					}
				}else{
					alreadyBound[varStr] = queChld[i];
				}
				// var is placeholder
			}else if( !(ruleChld[i].Equals(queChld[i]) ) ){
				return false; // atom not same
			}
		}
		return true;
	}
	
	public virtual Dictionary<string,Object> unify(Object queObj){
		var vars = new Dictionary<string,Object>();
		if( unify(queObj, this.Src, vars) ){
			return vars;
		}
		return null;
	}
	
	public List<RewriteResult> findReplace(Object queObj){
		var resList = new List<RewriteResult>();
		findReplace(queObj, this, resList);
		return resList;
	}
			

	// just replace, without checking for conditions
	// conditions must be checked by calling code if replace result is interesting
	public	static void findReplace(Object queObj, Rewrite rewr, List<RewriteResult> resList){
		var unifyVars = rewr.unify(queObj);
		if( unifyVars!=null ){
			//Console.WriteLine("unif vars "+vars);
			resList.Add( new RewriteResult( replaceVars(unifyVars, rewr.Target), unifyVars) );
			/*
			if( rewr.checkCondition(deduct, vars, withConditions) ){
			  return replaceVars(vars, rewr.Target);
			}
			*/
		}else if( !(queObj is Node) ){
			if( queObj.Equals(rewr.Src) ){
			  resList.Add( new RewriteResult( rewr.Target, new Dictionary<string,Object>()) );
				/*
  			  if( rewr.checkCondition(deduct, vars, withConditions) ){
			    return rewr.Target;
			  }
			  */
			}
		}
		if( queObj is Node ){
			Node que = (Node)queObj;
			for(int i=0; i<que.Children.Count; i++){
				Object ch = que.Children[i];
				List<RewriteResult> rrListChild = rewr.findReplace(ch);
				foreach(var rr in rrListChild){
					Node newMe = new Node(que.Name);
					for(int j=0; j<que.Children.Count; j++){
						newMe.add( j==i ? rr.Res : que.Children[j] );
					}
					// one place of unification is found - others are possible but 
					// that's enough for today - return replacement 
					rr.Res = newMe;
					resList.Add( rr );
				}
			}
		}
	}

	public static string dictVarsToString(Dictionary<string,Object> vars){
		string s = "";
		foreach(var e in vars){
			s += e.Key+"="+Node.nodeString(e.Value)+" ";
		}
		return s;
	}
	
	public static Object replaceVars(Dictionary<string,Object> vars, Object expr){
		if( isVar(expr) ){
			return vars[(string)expr];
		}else if( expr is string ){
			return expr;
		}
		Node n = (Node)expr;
		Node newN = new Node(n.Name);
		bool anyChange=false;
		for( int i=0; i<n.Children.Count; i++ ){
			Object repl = replaceVars(vars, n.Children[i]);
			newN.add(repl);
			if( repl!=n.Children[i] ){
				anyChange=true;
			}
		}
		if( anyChange ){
			return newN;
		}else{
			return n;
		}
		
	}
	
	

}
